(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 20))
(declare-fun v1 () (_ BitVec 20))
(assert (let ((e2(_ bv1703101337 32)))
(let ((e3 (bvsub e2 ((_ zero_extend 12) v0))))
(let ((e4 (bvnor ((_ zero_extend 12) v0) e2)))
(let ((e5 (ite (distinct e2 e3) (_ bv1 1) (_ bv0 1))))
(let ((e6 (bvshl e2 ((_ sign_extend 12) v1))))
(let ((e7 (bvsge e6 ((_ sign_extend 12) v1))))
(let ((e8 (= v0 ((_ zero_extend 19) e5))))
(let ((e9 (bvsgt e6 e3)))
(let ((e10 (distinct e2 e6)))
(let ((e11 (bvugt e3 e3)))
(let ((e12 (bvsgt e6 e4)))
(let ((e13 (ite e10 e9 e9)))
(let ((e14 (not e12)))
(let ((e15 (ite e11 e7 e11)))
(let ((e16 (not e14)))
(let ((e17 (xor e16 e16)))
(let ((e18 (ite e13 e17 e15)))
(let ((e19 (or e18 e8)))
e19
)))))))))))))))))))

(check-sat)
